Java Modeling Language
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
top
The Java Modeling Language (JML) is a specification language for Java
follows the design by contract paradigm. Specifications are written as
Java annotation comments to the source files, which hence can be
compiled with any Java compiler.
Various verification tools, such as a runtime assertion checker and the
Extended Static Checker (ESC/Java) aid development.
Contents
• Overview
• Syntax
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Overview
JML is a behavioural interface specification language for Java modules.
JML provides semantics to formally describe the behavior of a Java
module, preventing ambiguity with regard to the module designers'
Refinement Calculus, with the goal of providing rigorous formal
semantics while still being accessible to any Java programmer. Various
tools are available that make use of JML's behavioral specifications.
Because specifications can be written as annotations in Java program
files, or stored in separate specification files, Java modules with JML
specifications can be compiled unchanged with any Java compiler.
Syntax
JML specifications are added to Java code in the form of annotations in
comments. Java comments are interpreted as JML annotations when they
begin with an @ sign. That is, comments of the form
//@ <JML specification>
or
/*@ <JML specification> @*/
Basic JML syntax provides the following keywords
requires
Defines a precondition on the method that follows.
ensures
Defines a postcondition on the method that follows.
signals
Defines a postcondition for when a given Exception is thrown by the
method that follows.
signals_only
Defines what exceptions may be thrown when the given precondition
holds.
assignable
Defines which fields are allowed to be assigned to by the method that
follows.
pure
Declares a method to be side effect free (like assignable \nothing
but can also throw exceptions). Furthermore, a pure method is supposed
to always either terminate normally or throw an exception.
invariant
Defines an invariant property of the class.
loop_invariant
Defines a loop invariant for a loop.
also
Combines specification cases and can also declare that a method is
inheriting specifications from its supertypes.
assert
Defines a JML assertion.
spec_public
Declares a protected or private variable public for specification
purposes.
Basic JML also provides the following expressions
\result
An identifier for the return value of the method that follows.
\old(<expression>)
A modifier to refer to the value of the <expression> at the time of
entry into a method.
(\forall <decl>; <range-exp>; <body-exp>)
The universal quantifier.
(\exists <decl>; <range-exp>; <body-exp>)
a ==> b
a implies b
a <== b
a is implied by b
a <==> b
a if and only if b
as well as standard Java syntax for logical and, or, and not. JML
annotations also have access to Java objects, object methods and
operators that are within the scope of the method being annotated and
that have appropriate visibility. These are combined to provide formal
specifications of the properties of classes, fields and methods. For
example, an annotated example of a simple banking class may look like
public class BankingExample
{
public static final int MAX_BALANCE = 1000;
private /*@ spec_public @*/ int balance;
private /*@ spec_public @*/ boolean isLocked = false;
//@ public invariant balance >= 0 && balance <= MAX_BALANCE;
//@ assignable balance;
//@ ensures balance == 0;
public BankingExample()
{
this.balance = 0;
}
//@ requires 0 < amount && amount + balance < MAX_BALANCE;
//@ assignable balance;
//@ ensures balance == \old(balance) + amount;
public void credit(final int amount)
{
this.balance += amount;
}
//@ requires 0 < amount && amount <= balance;
//@ assignable balance;
//@ ensures balance == \old(balance) - amount;
public void debit(final int amount)
{
this.balance -= amount;
}
//@ ensures isLocked == true;
public void lockAccount()
{
this.isLocked = true;
}
//@ requires !isLocked;
//@ ensures \result == balance;
//@ also
//@ requires isLocked;
//@ signals_only BankingException;
public /*@ pure @*/ int getBalance() throws BankingException
{
if (!this.isLocked)
{
return this.balance;
}
else
{
throw new BankingException();
}
}
}
Full documentation of JML syntax is available in the JML Reference
Manual.
Tool support
A variety of tools provide functionality based on JML annotations. The
Iowa State JML tools provide an assertion checking compiler jmlc which
converts JML annotations into runtime assertions, a documentation
generator jmldoc which produces Javadoc documentation augmented with
extra information from JML annotations, and a unit test generator
jmlunit which generates JUnit test code from JML annotations.
Independent groups are working on tools that make use of JML
annotations. These include:
• ESC/Java2 [1], an extended static checker which uses JML annotations
to perform more rigorous static checking than is otherwise possible.
• OpenJML declares itself the successor of ESC/Java2.
• Daikon, a dynamic invariant generator.
• KeY, which provides an open source theorem prover with a JML front-end
and an Eclipse plug-in (JML Editing) with support for
syntax highlighting of JML.
• Krakatoa, a static verification tool based on the Why verification
platform and using the Coq proof assistant.
• JMLEclipse, a plugin for the Eclipse integrated development
environment with support for JML syntax and interfaces to various tools
that make use of JML annotations.
• Sireum/Kiasan, a symbolic execution based static analyzer which
supports JML as a contract language.
• JMLUnit, a tool to generate files for running JUnit tests on JML
annotated Java files.
• TACO, an open source program analysis tool that statically checks the
compliance of a Java program against its Java Modeling Language
specification.
References
• Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft
tutorial.
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for
Detailed Design; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds
(editors), Behavioral Specifications of Businesses and Systems, Kluwer,
1999, chapter 12, pages 175-188.
• Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby,
David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M.
Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML
• Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel.
Formal specification with JML. 2014. download (CC-BY-NC-ND)
External links